COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	term	::= var
C00003 00003	unify[x:termsy:termsz:subs]answer
C00005 ENDMK
C⊗;
term	::= var
	::= f_app

f_app	::= struct[n:f_name;a:terms]

f_name	::= id

terms	::= seq[term]

subs	::= seq[sub]

sub	::= struct[n:var;b:term]

answer	::= boolean
	::= subs
unify[x:terms;y:terms;z:subs]answer
 on(x,y)
	[ε,ε] => z
	[(r⊗s),(t⊗u)] =>{generic(unify1(r,t,z))
			    [boolean] => FALSE;
			    [subs(v)] => unify1(s,u,v)}}

	FALSE;
 end;

unify1[t:term;u:term;z:subs]answer
 generic(a:subst(t,z),b:subst(u,z))
	[var,var] => compose(z,a,b)
	[var,f_app(*,c)] => {occ_list(a,c) => FALSE;compose(z,a,c)}
	[f_app(*,c),var] => {occ_list(b,c) => FALSE;compose(z,b,c)}
	[f_app(f,c),f_app(g,d)] => {f≠g => FALSE;unify(c,d,z)}
 end;

subst[t:term;z;subs]term
 generic(t)
	[var] => subv(t,z)
	[f_app(u,v)] => f_app(u,su_list(v,z))
 end;

subv[x:var;z;subs]term
 on(z)
	[ε] => x
	[(sub(n,v)⊗z1)] => {x=n => v; subv(x;z1)}
 end;

su_list[x;terms;z:subs]terms
 on(x)
	[ε] => ε
	[(u⊗v)] => terms(subst(u,z)⊗su_list(v,z))
 end;

occur[x:var;t:term]boolean
 generic(t)
	[var] =>x=t
	[f_app(*,v)] => occ_list(x,v)
 end;

occ_list(x:var;y:terms) boolean
 on(y)
	[ε] => TRUE
	[(u⊗v)] =>{occur(x,u) => TRUE;occ_list(x,v)}
 end;

compose[z:subs;v:var;t:term]subs
 on(z)
	[ε] => subs(sub(v,t))
	[(sub(u,a)⊗z1)] => {u=v =>LOSS;
			      subs(sub(u,subst(a,subs(sub(v,t)))),
				compose(z1,v,t))}
 end;